Specification caterpillar-asm

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

data asm specification 
   caterpillar

   using list-prefixn
, 
         nat-mult


   

   
   
   
   
   procedures caterpillar_init# nat :  : nat × list × nat × list  ;
              caterpillar_add# elem × nat : list × nat × list nonfunctional ;
              caterpillar_get# nat × list × list :  : list  ;
   variables  h : nat;
              xs_len : nat;
              xs : list;
              ys : list;
   
   

   

   state variables  h : nat;
                    xs : list;
                    xs_len : nat;
                    ys : list;

   initialization procedure caterpillar_init#

   

   sequential

      invariants xs-size :  ⊦ # xs < h;
                 xs-length :  ⊦ # xs = xs_len;
                 ys-length :  ⊦ # ys = 0 ∨ # ys = h;
   
      

   

   

   

   

   

   

   

   

   

   

   declarations init:caterpillar_init#(n; ; h, xs, xs_len, ys)  precondition n > 0;{h := n, xs := [], xs_len := 0, ys := []}
                add:
                caterpillar_add#(a, h; xs, xs_len, ys)
                {if xs_len + 1 = h then {ys := a + xs; xs_len := 0; xs := []} else {xs := a + xs; xs_len := 1 + xs_len}
                }
                get:caterpillar_get#(h, xs, ys; ; x){x := prefixn(h, xs + ys)}
end data asm specification